T:Type, P:((T List)prop{i:l}).
(L:(T List). decidable(P(L)))
 (L:(T List). decidable((L':T List. (iseg(T; L'; L)  P(L'))))) 

latex

Definitions	t  T, prop{i:l}, x(s), x:A. B(x), decidable(P), iseg(T; l1; l2), P  Q, x:A. B(x), P  Q, firstn(n; as), ||as||, int_seg(i; j), P  Q, P  Q, ge(i; j), False, A, A  B, lelt(i; j; k), top, subtype(S; T), x. t(x)
Lemmas	decidable functionality, decidable ex int seg, firstn is iseg, firstn append, firstn length, top wf, iseg length, non neg length, iseg wf, int seg wf, length wf1, firstn wf, decidable wf